g:GrpSig, a, b:|g|. (a < b)   

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, gset, OMon, goset, a < b
Definitions	t.1, gset, |p|, goset, a < b, t  T, x:A. B(x)
Lemmas	grp sig wf, grp car wf, oset of ocmon wf0, set blt wf